#include <stdio.h>  // for FILE, fread
#include <ctype.h>  // for isalnum
#include <wchar.h>  // for wchar_t
#include <stddef.h> // for size_t
namespace unix_StdCLibraryFunctions {
#define EOF -1
void test_alnum_concrete(int v) {
    int ret = isalnum(256); // \
    // warning: Function argument outside of allowed range
    (void)ret;
}

void buffer_size_violation(FILE* file) {
    enum { BUFFER_SIZE = 1024 };
    wchar_t wbuf[BUFFER_SIZE];

    const size_t size = sizeof(*wbuf);   // 4
    const size_t nitems = sizeof(wbuf);  // 4096

    // Below we receive a warning because the 3rd parameter should be the
    // number of elements to read, not the size in bytes. This case is a known
    // vulnerability described by the ARR38-C SEI-CERT rule.
    fread(wbuf, size, nitems, file);
}

int test_alnum_symbolic(int x) {
    int ret = isalnum(x);
    // after the call, ret is assumed to be in the range [-1, 255]

    if (ret > 255)      // impossible (infeasible branch)
        if (x == 0)
            return ret / x; // division by zero is not reported
    return ret;
}
}